Nuprl Lemma : existse-rcv_wf
11,40
postcript
pdf
es
:ES,
l
:IdLnk,
tg
:Id,
P
:({
e
:E|
isrcv(
e
)}
). (
e
=rcv(
l
,
tg
).
P
(
e
))
latex
Definitions
t
T
,
E
,
b
,
x
:
A
.
B
(
x
)
,
,
x
(
s
)
,
rcv(
l
,
tg
)
,
kind(
e
)
,
Knd
,
A
c
B
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
e
=rcv(
l
,
tg
).
P
(
e
)
,
ES
,
IdLnk
,
Id
,
isrcv(
e
)
,
True
,
isrcv(
k
)
,
{
T
}
,
P
Q
,
SQType(
T
)
Lemmas
Knd
sq
,
assert
wf
,
es-isrcv
wf
,
Id
wf
,
IdLnk
wf
,
event
system
wf
,
es-E
wf
,
Knd
wf
,
es-kind
wf
,
rcv
wf
origin
es:ES, l:IdLnk, tg:Id, P:({e:E| 
isrcv(e)} 
). (
e=rcv(l,tg). P(e)) 
es:ES, l:IdLnk, tg:Id, P:({e:E| isrcv(e)} ). (e=rcv(l,tg). P(e)) Tbx:A. B(x)
Bx:A. B(x)e=rcv(l,tg). P(e)
Q